ds:x:Id fp Type, da:k:Knd fp Type, A:ecl-trans-tuple{i:l}(ds;da), n:.
ecl-trans-act(ds;da;A)(n,nil)  False 

latex

Definitions

P  Q, False, A, AB, , P & Q, t  T, x:A. B(x), event-info(ds;da), P  Q, x:A. B(x), b, ecl-trans-act(ds;da;A), Id, x. t(x), a:A fp B(a), Knd, ecl-trans-tuple{i:l}(ds;da), P  Q, Dec(P), P  Q, Prop, (x  l), ||as||, Y, l[i], hd(l), nth_tl(n;as), if b t else f fi, ij, b, i<j, tl(l), IdLnk, State(ds), f(x)?z, x  dom(f), deq-member(eq;x;L), reduce(f;k;as), p  q, eqof(d), 1of(t), f(x), 2of(t), IdDeq, product-deq(A;B;a;b), proddeq(a;b), p  q, prod-deq(A;B;a;b), AtomDeq, x=yAtom, atom-deq-aux, NatDeq, i=j, Top, KindDeq, union-deq(A;B;a;b), sumdeq(a;b), sum-deq(A;B;a;b), IdLnkDeq

Lemmas

decidable false, ecl-trans-act wf, false wf, nat wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, append is nil, event-info wf